(asdf:operate 'asdf:load-op 'ezot)
(use-package :trio-utils)

(defvar BOUND    15)
(defvar TMODE   '(NC C B))	;;torqueMode
(defvar DMODE   '(D R P N))	;;driveMode
;;(defvar DMODE   '(P))	;; use this is you want to force a particular driveMode
;; this is useful to generate specific models

;;engine rpm (in_rpm) are between 1000 and 6000
;;below 1300 rpm the engine is disconnected
(defvar RPM '(0 0.5 1 1.1 1.2 1.3 1.4 1.5 1.6 1.7 1.8 1.9 2 3 4 5 6 7 8);;*1000

(define-variable rpm_in RPM)	;;rpm_in (from engine)
(define-variable rpm_out RPM)	;;rpm_out (to planetary gear sets)
(define-variable sm TMODE)	;;selectedTorqueMode
(define-variable cm TMODE)	;;currentTorqueMode
(define-variable dm DMODE)	;;driveMode

;;   ---axioms---

;;*see: Engine.Min_Limit_For_Rpm and Engine.Max_Limit_For_Rpm
(defvar rpm_in_engine_bound (-E- x RPM (&& (>= x 1) (<= x 5) (rpm_in-is x))))

(defvar ex_dm (-E- x DMODE(dm-is x))) 	;; one and only one values for dm
;;this is not necessary for others because they are setted as a consequence
;;of dm and rpm_in. Also rpm_in as been already setted.
;;rpm_out can have multiple values, this is not a problem for this model 

;;*see: TorqueConverter.Selected_Current_TorqueMode
(defvar sc_linkC (<->
	(&&(sm-is 'C)(-E- x RPM (&& (>= x 1.3)(rpm_in-is x))))
	(cm-is 'C)))
(defvar sc_linkNC (<->
	(||
		(sm-is 'NC)
		(&&(sm-is 'C)(-E- x RPM (&& (< x 1.3)(rpm_in-is x)))))
	(cm-is 'NC)))
(defvar sc_linkB (<->(sm-is 'B)(cm-is 'B)))

;;*see: ModeSelector.Communication_of_User_change_to_all
(defvar ds_linkN (<->
	(dm-is 'N)(sm-is 'NC)))
(defvar ds_linkP (<->
	(dm-is 'P)(sm-is 'B)))
(defvar ds_linkDR (<->
	(||(dm-is 'D)(dm-is 'R))(sm-is 'C)))

;;*see TorqueConverter.Connected_Normal_Behavior
(defvar Connected(->(cm-is 'C)
	(-E- x RPM (&&( rpm_in-is x) (rpm_out-is x)))))
;;*see TorqueConverter.Blocked_Behavior
(defvar Blocked(->(cm-is 'B)
	(-E- x RPM (&&(= x 0) (rpm_out-is x)))))


;;   ---theorems---
  
;;(defvar tautology (<->(-P- t) (-P- t)))

(defvar not_connected_if_low_rpm_in_or_low_rpm_out
	(->(-E- x RPM (&&(< x 1.3)(||(rpm_in-is x)(rpm_in-is x))))(!!(cm-is 'C))))
	
(defvar  low_or_high_rpm_out_only_if_not_connected
	(<-(cm-is 'NC)
	(-E- x RPM (&&(||(< x 1.3)(> x 6))(!!(= x 0))(rpm_out-is x)))))
	
(defvar car_moving_if_DorR
	(->(&&(||(dm-is 'D)(dm-is 'R))(-E- x RPM(&&(>= x 1.3)(rpm_in-is x))))
	(-E- x RPM (&&(>= x 1)(rpm_out-is x)))))
	
(defvar car_blocked_if_P
	(->(dm-is 'P)
	(-E- x RPM (&&(= x 0)(rpm_out-is x)))))



(defvar whole_system (alw (&& 
	rpm_in_engine_bound ex_dm
	ds_linkN ds_linkP ds_linkDR
	sc_linkC sc_linkNC sc_linkB	
	Connected Blocked)))


;;   ---verification---
;;only one of the following lines should be uncommented


;;uncomment this to check the SATISFIABILITY of the model
(ezot:zot BOUND whole_system )


;; do not use these lines
;;(ezot:zot BOUND (&& whole_system not_connected_if_low_rpm_in_or_low_rpm_out))
;;(ezot:zot BOUND (&& whole_system low_or_high_rpm_out_only_if_not_connected))
;;(ezot:zot BOUND (&& whole_system car_moving_if_DorR))
;;(ezot:zot BOUND (&& whole_system car_blocked_if_P))


;; uncomment the following lines to check the corresponding theorems
;; theorem is true iif new model is UNSATISFIABLE (and standard model is SATISFIABLE)
;;(ezot:zot BOUND (&& whole_system (!! not_connected_if_low_rpm_in_or_low_rpm_out)))
;;(ezot:zot BOUND (&& whole_system (!! low_or_high_rpm_out_only_if_not_connected)))
;;(ezot:zot BOUND (&& whole_system (!! car_moving_if_DorR)))
;;(ezot:zot BOUND (&& whole_system (!! car_blocked_if_P)))
